feat(fc): prove pruning preserves the fork-choice head and finalized checkpoint - #76

…tally

Deliver the weight-delta layer of #67: the algebraic core that makes
proto-array-style incremental head computation a refinement of the
naive spec walk.

- Weights.Equiv: extensional equality of weight maps, with get_bump
  characterizing bump as pointwise +1.
- creditChain_get_add / accumulateAncestorWeights_append: the vote
  tally is pointwise additive, so per-vote weight deltas are
  well-defined.
- accumulateAncestorWeights_perm: the tally is order-free — an
  incremental maintainer may apply vote updates in any order.
- ghostWalk_congr_weights / computeLmdGhostHead_incremental: the GHOST
  descent (children, threshold, comparison, tie-break) reads weights
  only through get, so any maintained map extensionally equal to the
  full tally selects exactly the spec head.

creditChain is made public (was private) so the lemmas can reason
about each step, mirroring the ghostWalk precedent.

The best-child/best-descendant cache layer of proto-array sits on top
and is follow-up; its correctness reduces to the walk over the same
weight function proved here.

Deliver the invariant half of #71 on top of the memory bound:

- getBlock?_prune_iff / getState?_prune_iff: lookups on the pruned
  store return the original entry exactly when pruning keeps it
  (via an association-list find?/filter characterization under key
  uniqueness).
- ancestorWalk_sound: walk success exhibits the relational ancestry
  plus the ancestor block at the checkpoint slot (converse of
  ancestorWalk_complete).
- keepBlock_of_ancestorOrEqual: every finalized-subtree block
  survives pruning.
- properAncestor_prune: finalized-rooted ancestry derivations
  transfer to the pruned store (each visited node is kept).
- prune_wellFormed: pruning preserves WellFormed. The justified
  anchor survives with its finalized ancestry: the justified root
  lies on the finalized subtree (M-1), the transferred relation is
  re-run by walk completeness inside the pruned store via an
  auxiliary store whose justified checkpoint is the finalized one
  (breaking the WellFormed circularity), and congruence maps the
  result back.

Deliver the head half of #71's observational equivalence:
updateHead_head_prune — for any WellFormed store,
(updateHead (prune st)).head = (updateHead st).head.

Proof structure:
- Subtree closure: ancestors of kept blocks at or above the finalized
  slot are kept (keepBlock_of_chain, via ancestor comparability); no
  ancestor of an off-subtree block is kept (keepBlock_off_chain).
- Vote weights agree on the subtree (KeptAgree): an on-subtree vote
  credits an identical chain in both stores
  (creditChain_prune_keptAgree); an off-subtree vote credits only
  off-subtree blocks in the full store (creditChain_get_off) and
  nothing in the pruned store.
- The GHOST walk reads only the subtree: children of kept blocks are
  the same list in both stores (childrenOf_prune, filter absorption),
  and all weight comparisons happen at kept roots (ghostWalk_prune).
- Fuel stability: both walks are driven by blocks.length + 1, which
  shrinks under pruning; the walks visit only kept blocks at strictly
  monotone slots, so any fuel above the subtree size gives the same
  result (creditChain_fuel_stable, ghostWalk_fuel_stable, with
  keptBelow/keptAbove as decreasing measures).

The finalized-checkpoint half of update_head (descendToSlot
re-derivation) is follow-up: it interacts with the reorg-mutable
latest_finalized (leanEthereum/leanSpec#1176 M-3), since a head state
may finalize below the pruning horizon.

Branch merges feat/fc-incremental-weights for Weights.get_bump.

Complete #71's observational equivalence of update_head:

updateHead_prune — for any WellFormed store whose stored states never
finalize below the store's finalized checkpoint, pruning changes
neither the selected head nor the re-derived finalized checkpoint.

- finalizeAt / descendToSlot_stop: the checkpoint derivation as a
  function of the walk landing.
- descend_finalize_prune: the re-derivation walks may genuinely
  diverge — when the head chain jumps past the target slot into
  pruned territory, the full store descends one block further than
  the pruned store — but both landings then miss the exact-slot
  check, so the derived checkpoint agrees (the interesting case of
  the equivalence).
- updateHead_latestFinalized_eq: definitional reduction of the
  latestFinalized field to finalizeAt over the walk.

The monotonicity hypothesis is the fork-choice face of
leanEthereum/leanSpec#1176 M-3 (latest_finalized is reorg-mutable):
it is exactly the condition a pruning client must ensure, mirroring
consensus-specs' monotone update_checkpoints. The proof surfaces M-3
as the precise boundary of pruning safety.